docs: author the proof-needs inventory (P-/F-/K- obligation series)#609
Merged
Conversation
Replace the near-empty PROOF-NEEDS.md (which held only the 2026-03-29
template-ABI cleanup note) with a real, structured inventory of what
AffineScript must prove, at what rigour, with honest status.
Three partitions, answering the "what did we miss" review directly:
P-1..P-10 Pre-faces obligations that existed but were never catalogued
— solo-core is statements-only (Step has no constructors;
progress/preservation are ?todo holes), the seven academic
proofs are prose, mechanized/ is stubs, formal/ is absent,
and the open soundness holes (#554/#555/#556/#558/#559) had
no proof obligations linking them to the soundness arguments
they falsify.
K-1..K-4 Needs sharpened by outstanding work — codegen semantic-
preservation (#513 #7) is the keystone every face rests on;
effect-soundness is *blocked* (not merely unproven) by #555;
borrow soundness must be stated to reject #554.
F-1..F-7 NEW obligations from the faces work, entirely absent from the
#513 programme: transformer semantics-preservation (the real
same-cube theorem), same-cube cross-face agreement (partially
mechanized in invariant-path/proofs/SameCube.agda; divergence
instance #601), pragma-detection determinism, error-vocabulary
faithfulness, render_ty non-collision, preview round-trip,
face confluence.
Also catalogues the aggregate-library law-conformance obligation and points
the same-cube track at invariant-path's SameCube.agda + verify-same-cube.sh.
Rename .md -> .adoc per DOC-FORMAT; update the three referrers (NAVIGATION,
verisimdb integration, FRG-PROFILE) — FRG-PROFILE's "no PROOF-NEEDS" honest
gap is now met (path-to-D step 6 done; grade unchanged, still no formal/).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
🔍 Hypatia Security ScanFindings: 43 issues detected
View findings[
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (32 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (29 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
🔍 Hypatia Security ScanFindings: 43 issues detected
View findings[
{
"reason": "Action denoland/setup-deno@v2 needs attention",
"type": "unpinned_action",
"file": "publish-jsr.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
"type": "js_exec_sync",
"file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "expect() in hot path (32 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "expect() in hot path (29 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
"type": "unsafe_block",
"file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
added a commit
that referenced
this pull request
Jun 21, 2026
## What Merges current `main` into `feat/solo-core-metatheory-proofs` and resolves all conflicts, so that **#614 stops being `mergeable_state: dirty`**. While #614 is dirty, GitHub cannot build the merge commit, so its entire CI suite is suppressed (only `lint-workflows` runs). Merging this PR into the feature branch un-blocks #614's CI. ## Why it was needed #614 branched off an old `main` (merge-base 61 commits back) and conflicts with the standalone-CI + codegen work that has since landed (#602, #603, #604, #606, #609, #610, #611, #612, #613). ## Conflict resolutions (5 files) | File(s) | Resolution | |---|---| | `governance.yml`, `scorecard.yml`, `scorecard-enforcer.yml`, `hypatia-scan.yml` | Take `main`'s **standalone** versions. The branch re-adopted the estate `standards` reusables that `main` deliberately dropped (#603/#604) to stop run-creation `startup_failure`s. `main`'s `hypatia-scan.yml` also restores the permissions Hypatia needs (`security-events: write`, `pull-requests: write`, `secrets: inherit`) and the `MPL-2.0` SPDX id the Palimpsest license doc mandates for tooling. | | `docs/PROOF-NEEDS.md` | Drop the branch's stale 103-line `.md`; keep `main`'s canonical 359-line `.adoc` (#609). Also satisfies DOC-FORMAT. | | `docs/history/MODULE-SYSTEM-PROGRESS` | Keep the branch's `.md`→`.adoc` migration; **port** `main`'s additive #138 codegen-follow-up note + status-table row into the `.adoc` so `main`'s work is preserved. | `spark-theatre-gate.yml` and `mirror.yml` were identical to `main`. ## Verification (merged tree) - `dune build` — clean - `dune test` — **534/534 pass** (incl. `cross-module constructor linking, Wasm (#138)`, `Wasm nested tuple patterns`, `Deno-ESM / JS no duplicate Option/Result constructor`) - wasm-runtime harness (`tools/run_codegen_wasm_tests.sh`) — all pass - workflow scan — no `startup_failure` risk introduced ## How to use Merge this into `feat/solo-core-metatheory-proofs`. #614 then becomes mergeable and its full CI runs. > Routed via this branch because the environment only permits pushes to `claude/inspiring-newton-dg5wov`, not directly to the feature branch. Un-blocks #614. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8 --- _Generated by [Claude Code](https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8)_ --------- Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: hyperpolymath <paraordinate@yahoo.co.uk>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Replaces the near-empty
docs/PROOF-NEEDS.md(which held only the 2026-03-29 template-ABI cleanup note) with a real, structured inventory of what AffineScript must prove, at what rigour, with honest status — and renames it to.adocper DOC-FORMAT.This is the deliverable for a fresh proof-needs review of the repo: what we may have missed before, what's sharpened by outstanding work, and what's newly arisen from the faces work.
The review, in three partitions
P-1…P-10— pre-faces obligations that existed but were never catalogued. The mechanized core is thinner than the prose corpus suggests:solo-core/Soundness.idris statements-only —data Stephas no constructors,progress/preservationare?todoholes. It proves nothing yet, and covers only the Solo fragment (no traits/effects/rows/refinements/ownership/dependent types).docs/academic/proofs/*.mdare prose;docs/academic/mechanized/{agda,coq,lean}/are explicit stubs; theaffinescript-vite/verification/proofs/files are RSR templates; andformal/(the dir Umbrella: 8 must-have + 12 high-priority proof obligations for the AffineScript compiler #513 names) does not exist.K-1…K-4— needs sharpened by outstanding work. Codegen semantic-preservation (#513 must-have 7) is the keystone every face rests on; effect-soundness is blocked (not merely unproven) by the #555 handler mis-lowering; borrow soundness must be stated to reject the #554 counterexample.F-1…F-7— NEW obligations from the faces work, entirely absent from the #513 programme:invariant-path/proofs/SameCube.agda(unit-tail case); the value-returning divergence is the concrete instance Face transformers disagree on trailing-statement lowering —greetcompiles to 2 wasm classes #601lib/face_pragma.ml)lib/face.ml— a simulation, beyond OCaml's exhaustiveness check)render_tyinjectivity / non-collisionAlso catalogues the aggregate-library law-conformance obligation (cross-cube, vs faces' cross-face) and points the same-cube track at invariant-path's
SameCube.agda+verify-same-cube.sh.Also in this PR
docs/PROOF-NEEDS.md→docs/PROOF-NEEDS.adoc(DOC-FORMAT).docs/NAVIGATION.adoc,.machine_readable/integrations/verisimdb.a2ml, andspec/FRG-PROFILE.adoc— the FRG "no PROOF-NEEDS" honest gap is now met (path-to-D step 6 done; grade unchanged, still noformal/prover encoding).Scope / non-goals
This is a catalogue of obligations only — no proof is asserted discharged, no code changes, no relicensing. Every
Statuscolumn entry ofstated/prose/absentmeans not proven. Cross-referenced to #513 (it adds the faces + aLib obligations #513 omits) and #563.🤖 Generated with Claude Code
https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
Generated by Claude Code